----------------------------- MODULE MemoryManager -----------------------------

EXTENDS Naturals, Sequences, FiniteSets

(*
 * ZENrs 内存管理器形式化模型
 * 
 * 本模型描述了ZENrs exokernel中内存管理器的关键属性和行为，
 * 用于验证内存分配、释放和映射操作的正确性和安全性。
 *)

(* 类型定义 *)
PhysicalAddress == Int
VirtualAddress == Int
MemorySize == Int
PageSize == 4096

(* 内存区域类型 *)
MemoryRegionType == {"free", "reserved", "acpi_reclaimable", "acpi_nvs", "bad_memory"}

(* 内存区域 *)
MemoryRegion == [
    base : PhysicalAddress,
    size : MemorySize,
    type : MemoryRegionType
]

(* 物理内存块 *)
PhysicalMemoryBlock == [
    base : PhysicalAddress,
    size : MemorySize,
    free : Bool
]

(* 内存权限 *)
MemoryPermissions == [
    read : Bool,
    write : Bool,
    execute : Bool
]

(* 内存映射 *)
MemoryMapping == [
    virt_addr : VirtualAddress,
    phys_addr : PhysicalAddress,
    size : MemorySize,
    perms : MemoryPermissions
]

(* 内存管理器状态 *)
MemoryManagerState == [
    memory_regions : Seq(MemoryRegion),
    free_blocks : Seq(PhysicalMemoryBlock),
    mappings : Seq(MemoryMapping),
    page_size : MemorySize
]

(* 初始状态 *)
Init == LET
    (* 初始内存区域 *)
    initialRegions == [
        [base |-> 1048576, size |-> 15728640, type |-> "free"],  (* 1MB-16MB 可用区域 *)
        [base |-> 15728640, size |-> 1048576, type |-> "reserved"] (* 15MB-16MB 保留区域 *)
    ]
    
    (* 初始空闲块 *)
    initialFreeBlocks == [
        [base |-> 1048576, size |-> 15728640, free |-> TRUE]
    ]
IN
    [
        memory_regions |-> initialRegions,
        free_blocks |-> initialFreeBlocks,
        mappings |-> << >>,
        page_size |-> PageSize
    ]

(* 辅助函数：对齐大小到页边界 *)
AlignToPage(size) == (size + (PageSize - 1)) // PageSize * PageSize

(* 辅助函数：检查地址是否对齐 *)
IsAligned(addr, alignment) == addr % alignment = 0

(* 辅助函数：检查内存块是否重叠 *)
BlocksOverlap(block1, block2) == 
    LET
        end1 == block1.base + block1.size - 1
        end2 == block2.base + block2.size - 1
    IN
        block1.base <= end2 /\ block2.base <= end1

(* 分配物理内存 *)
AllocatePhysicalMemory(mms, size, alignment) == 
    LET
        aligned_size == AlignToPage(size)
        (* 查找合适的空闲块 *)
        found_block == CHOOSE i \in DOMAIN mms.free_blocks : 
            mms.free_blocks[i].free /\ mms.free_blocks[i].size >= aligned_size
        
        block == mms.free_blocks[found_block]
        aligned_addr == IF IsAligned(block.base, alignment) THEN 
            block.base 
        ELSE 
            block.base + (alignment - (block.base % alignment))
        
        alignment_padding == aligned_addr - block.base
        
        (* 更新状态 *)
        new_free_blocks == IF block.size - alignment_padding - aligned_size > mms.page_size THEN 
            (* 分割块 *)
            ReplaceAt(
                ReplaceAt(mms.free_blocks, found_block, 
                    [base |-> block.base, size |-> alignment_padding, free |-> TRUE]), 
                found_block + 1, 
                [base |-> aligned_addr + aligned_size, size |-> block.size - alignment_padding - aligned_size, free |-> TRUE]
            )
        ELSE 
            (* 不分割块 *)
            ReplaceAt(mms.free_blocks, found_block, 
                [base |-> aligned_addr, size |-> aligned_size, free |-> FALSE])
    IN
        [mms EXCEPT 
            !free_blocks = new_free_blocks
        ]

(* 释放物理内存 *)
FreePhysicalMemory(mms, addr, size) == 
    LET
        aligned_size == AlignToPage(size)
        (* 查找对应的块 *)
        found_block == CHOOSE i \in DOMAIN mms.free_blocks : 
            ~mms.free_blocks[i].free /\ mms.free_blocks[i].base = addr /\ mms.free_blocks[i].size = aligned_size
        
        (* 更新状态 *)
        new_free_blocks == IF found_block # "" THEN 
            ReplaceAt(mms.free_blocks, found_block, 
                [base |-> addr, size |-> aligned_size, free |-> TRUE])
        ELSE 
            mms.free_blocks
    IN
        [mms EXCEPT 
            !free_blocks = new_free_blocks
        ]

(* 映射内存 *)
MapMemory(mms, virt_addr, phys_addr, size, perms) == 
    LET
        new_mapping == [
            virt_addr |-> virt_addr,
            phys_addr |-> phys_addr,
            size |-> size,
            perms |-> perms
        ]
        
        new_mappings == Append(mms.mappings, new_mapping)
    IN
        [mms EXCEPT 
            !mappings = new_mappings
        ]

(* 解除内存映射 *)
UnmapMemory(mms, virt_addr, size) == 
    LET
        (* 查找对应的映射 *)
        found_mapping == CHOOSE i \in DOMAIN mms.mappings : 
            mms.mappings[i].virt_addr = virt_addr /\ mms.mappings[i].size = size
        
        (* 更新状态 *)
        new_mappings == IF found_mapping # "" THEN 
            SubSeq(mms.mappings, 1, found_mapping - 1) 
            \o SubSeq(mms.mappings, found_mapping + 1, Len(mms.mappings))
        ELSE 
            mms.mappings
    IN
        [mms EXCEPT 
            !mappings = new_mappings
        ]

(* 下一步状态关系 *)
Next(mms, mms') == 
    (* 内存分配操作 *)
    (\E size, alignment \in MemorySize : 
        mms' = AllocatePhysicalMemory(mms, size, alignment)
    ) \/ 
    
    (* 内存释放操作 *)
    (\E addr \in PhysicalAddress, size \in MemorySize : 
        mms' = FreePhysicalMemory(mms, addr, size)
    ) \/ 
    
    (* 内存映射操作 *)
    (\E virt_addr \in VirtualAddress, phys_addr \in PhysicalAddress, size \in MemorySize, perms \in MemoryPermissions : 
        mms' = MapMemory(mms, virt_addr, phys_addr, size, perms)
    ) \/ 
    
    (* 内存解除映射操作 *)
    (\E virt_addr \in VirtualAddress, size \in MemorySize : 
        mms' = UnmapMemory(mms, virt_addr, size)
    )

(* 系统行为 *)
Spec == Init /\ [][Next]_<<mms.memory_regions, mms.free_blocks, mms.mappings>>

(* 不变式：已分配的内存块不重叠 *)
NoOverlappingAllocatedBlocks == \A i, j \in DOMAIN mms.free_blocks : 
    i # j /\ ~mms.free_blocks[i].free /\ ~mms.free_blocks[j].free => 
        ~BlocksOverlap(mms.free_blocks[i], mms.free_blocks[j])

(* 不变式：所有映射的物理内存都是已分配的 *)
AllMappedMemoryIsAllocated == \A m \in mms.mappings : 
    \E b \in mms.free_blocks : 
        ~b.free /\ b.base <= m.phys_addr /\ m.phys_addr + m.size <= b.base + b.size

(* 不变式：已分配的内存大小不会超过总内存大小 *)
AllocatedMemoryDoesNotExceedTotal == 
    LET
        total_memory == Sum(r.size : r \in mms.memory_regions)
        allocated_memory == Sum(b.size : b \in mms.free_blocks, ~b.free)
    IN
        allocated_memory <= total_memory

(* 验证条件 *)
THEOREM MemoryManagerCorrectness == Spec => 
    []NoOverlappingAllocatedBlocks /\ 
    []AllMappedMemoryIsAllocated /\ 
    []AllocatedMemoryDoesNotExceedTotal

=============================================================================